 (set-logic QF_UFLIA)
 (declare-fun uf3 (Bool Bool Bool) Bool)
 (declare-fun uf4 (Bool Bool Bool Bool) Bool)
 (declare-fun uf7 (Bool Bool Bool Bool Bool Bool Bool) Bool)
 (declare-fun uf3_2 (Bool Bool Bool) Bool)
 (declare-fun uf4_2 (Bool Bool Bool Bool) Bool)
 (declare-fun v0 () Bool)
 (declare-fun v1 () Bool)
 (declare-fun v2 () Bool)
 (declare-fun v3 () Bool)
 (declare-fun v5 () Bool)
 (declare-fun v6 () Bool)
 (declare-fun v7 () Bool)
 (declare-fun v8 () Bool)
 (declare-fun i0 () Int)
 (declare-fun i1 () Int)
 (declare-fun i2 () Int)
 (declare-fun i3 () Int)
 (declare-fun i5 () Int)
 (declare-fun i7 () Int)
 (declare-fun i8 () Int)
 (declare-fun i9 () Int)
 (declare-fun ufib3 (Int Int Int) Bool)
 (declare-fun ufbi3 (Bool Bool Bool) Int)
 (declare-fun ufbi7 (Bool Bool Bool Bool Bool Bool Bool) Int)
 (declare-fun ufii5 (Int Int Int Int Int) Int)
 (declare-fun ufii6_2 (Int Int Int Int Int Int) Int)
 (declare-sort S0 0)
 (declare-fun i10 () Int)
 (assert (xor v7 v7))
 (declare-fun v9 () Bool)
 (declare-fun v10 () Bool)
 (declare-fun v11 () Bool)
 (push 2)
 (declare-fun v12 () Bool)
 (push 4)
 (declare-fun v13 () Bool)
 (declare-fun v14 () Bool)
 (declare-fun i11 () Int)
 (declare-fun v15 () Bool)
 (declare-fun v16 () Bool)
 (declare-fun v17 () Bool)
 (declare-fun v18 () Bool)
 (declare-fun v19 () Bool)
 (pop 2)
 (declare-fun v20 () Bool)
 (declare-fun v21 () Bool)
 (declare-fun i12 () Int)
 (declare-fun v22 () Bool)
 (declare-fun i13 () Int)
 (declare-fun v23 () Bool)
 (pop 3)
 (declare-fun v24 () Bool)
 (declare-fun v25 () Bool)
 (declare-fun i14 () Int)
 (declare-fun v26 () Bool)
 (declare-fun v27 () Bool)
 (pop 1)
 (declare-fun v28 () Bool)
 (declare-fun S0-0 () S0)
 (declare-fun v29 () Bool)
 (declare-sort S1 0)
 (declare-fun i15 () Int)
 (declare-fun v31 () Bool)
 (declare-fun i16 () Int)
 (declare-fun v32 () Bool)
 (declare-fun i17 () Int)
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 ) (2404 2363 110 539 982 3122 1137 3300 1776 2584 3961 1841 ))
 (declare-fun v34 () Bool)
 (declare-fun v35 () Bool)
 (push 3)
 (declare-fun v36 () Bool)
 (declare-fun v37 () Bool)
 (push 4)
 (declare-fun v38 () Bool)
 (declare-fun v39 () Bool)
 (declare-fun v40 () Bool)
 (declare-fun i18 () Int)
 (declare-fun v41 () Bool)
 (declare-fun v42 () Bool)
 (pop 7)
 (declare-fun v43 () Bool)
 (declare-fun v44 () Bool)
 (declare-fun v45 () Bool)
 (declare-fun i19 () Int)
 (declare-fun S1-0 () S1)
 (declare-fun v46 () Bool)
 (declare-fun v47 () Bool)
 (declare-fun i20 () Int)
 (push 1)
 (declare-fun v49 () Bool)
 (declare-fun i21 () Int)
 (declare-fun v50 () Bool)
 (declare-fun v51 () Bool)
 (pop 1)
 (declare-fun v52 () Bool)
 (declare-fun v53 () Bool)
 (push 1)
 (declare-fun v55 () Bool)
 (declare-fun i22 () Int)
 (pop 1)
 (declare-fun v57 () Bool)
 (declare-fun i23 () Int)
 (push 5)
 (declare-fun v58 () Bool)
 (pop 5)
 (declare-fun v59 () Bool)
 (declare-fun v61 () Bool)
 (declare-fun i24 () Int)
 (push 4)
 (declare-fun v62 () Bool)
 (declare-fun i25 () Int)
 (declare-fun v63 () Bool)
 (push 5)
 (declare-fun v64 () Bool)
 (declare-fun v65 () Bool)
 (declare-fun v66 () Bool)
 (push 4)
 (declare-fun v67 () Bool)
 (pop 12)
 (declare-fun v68 () Bool)
 (declare-fun i26 () Int)
 (declare-fun v69 () Bool)
 (push 4)
 (declare-fun v70 () Bool)
 (declare-fun i27 () Int)
 (push 4)
 (declare-sort S2 0)
 (declare-fun v71 () Bool)
 (push 1)
 (declare-fun S2-0 () S2)
 (declare-fun v72 () Bool)
 (declare-fun v73 () Bool)
 (push 3)
 (declare-fun v74 () Bool)
 (declare-fun v75 () Bool)
 (declare-fun v76 () Bool)
 (declare-fun i28 () Int)
 (push 3)
 (declare-fun v77 () Bool)
 (push 3)
 (declare-fun S1-1 () S1)
 (declare-fun v78 () Bool)
 (pop 17)
 (declare-fun v79 () Bool)
 (push 2)
 (declare-fun v80 () Bool)
 (declare-fun i29 () Int)
 (declare-fun v81 () Bool)
 (declare-fun v82 () Bool)
 (declare-fun v83 () Bool)
 (declare-fun v84 () Bool)
 (declare-fun v85 () Bool)
 (pop 3)
 (declare-fun v86 () Bool)
 (declare-fun v87 () Bool)
 (declare-fun i30 () Int)
 (declare-fun v88 () Bool)
 (declare-fun i31 () Int)
 (declare-fun v89 () Bool)
 (declare-fun i32 () Int)
 (push 2)
 (declare-fun v90 () Bool)
 (declare-fun v91 () Bool)
 (pop 1)
 (declare-fun v92 () Bool)
 (declare-fun v93 () Bool)
 (declare-fun i33 () Int)
 (pop 1)
 (push 5)
 (declare-fun v94 () Bool)
 (push 3)
 (declare-fun v95 () Bool)
 (declare-fun v96 () Bool)
 (declare-fun v97 () Bool)
 (declare-fun i34 () Int)
 (declare-fun v98 () Bool)
 (pop 2)
 (declare-fun v99 () Bool)
 (pop 2)
 (push 4)
 (declare-fun v100 () Bool)
 (declare-fun i35 () Int)
 (pop 4)
 (declare-fun v101 () Bool)
 (declare-fun i36 () Int)
 (pop 1)
 (push 3)
 (declare-fun v102 () Bool)
 (declare-fun i37 () Int)
 (pop 2)
 (declare-fun v103 () Bool)
 (declare-fun i38 () Int)
 (declare-fun v104 () Bool)
 (pop 1)
 (declare-fun v105 () Bool)
 (declare-fun v106 () Bool)
 (declare-fun v107 () Bool)
 (push 4)
 (declare-fun v108 () Bool)
 (declare-fun i39 () Int)
 (declare-fun v109 () Bool)
 (declare-fun v110 () Bool)
 (declare-fun i40 () Int)
 (declare-fun v111 () Bool)
 (declare-fun v112 () Bool)
 (push 3)
 (declare-fun v113 () Bool)
 (pop 7)
 (declare-fun v114 () Bool)
 (declare-fun v115 () Bool)
 (declare-fun v116 () Bool)
 (declare-fun i41 () Int)
 (declare-fun v117 () Bool)
 (check-sat-assuming-model (i1 i19 i30) (1988 3521 4514))
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i30 i31 i32 i41 ) (4627 3533 3390 3090 1029 3695 4232 2502 4031 2964 3214 365 539 3707 3005 1012 1555 4687 2473 2439 ))
 (declare-fun i42 () Int)
 (push 1)
 (declare-fun v118 () Bool)
 (declare-fun i43 () Int)
 (declare-fun v119 () Bool)
 (declare-fun i44 () Int)
 (declare-fun S0-1 () S0)
 (declare-fun v120 () Bool)
 (push 4)
 (declare-fun v121 () Bool)
 (declare-fun v122 () Bool)
 (declare-fun v123 () Bool)
 (declare-fun i45 () Int)
 (push 1)
 (declare-fun v124 () Bool)
 (push 4)
 (declare-fun v125 () Bool)
 (declare-fun i46 () Int)
 (declare-fun v126 () Bool)
 (declare-fun i47 () Int)
 (push 3)
 (declare-fun i48 () Int)
 (push 3)
 (declare-fun v127 () Bool)
 (declare-fun v128 () Bool)
 (pop 19)
 (declare-fun i49 () Int)
 (declare-fun v129 () Bool)
 (push 2)
 (declare-fun v130 () Bool)
 (push 4)
 (declare-fun v131 () Bool)
 (declare-fun i50 () Int)
 (pop 6)
 (declare-fun v132 () Bool)
 (push 1)
 (declare-fun v133 () Bool)
 (declare-fun v134 () Bool)
 (pop 1)
 (declare-fun i51 () Int)
 (check-sat-assuming-model (i9 i15 i23) (2890 170 1121))
 (declare-fun v135 () Bool)
 (push 3)
 (declare-fun i52 () Int)
 (declare-fun v136 () Bool)
 (declare-fun v137 () Bool)
 (push 5)
 (declare-fun v138 () Bool)
 (declare-fun i53 () Int)
 (pop 3)
 (declare-fun v139 () Bool)
 (declare-fun v140 () Bool)
 (push 2)
 (declare-fun v141 () Bool)
 (declare-fun v142 () Bool)
 (push 3)
 (declare-fun v143 () Bool)
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i30 i31 i32 i49 i51 i52 ) (1211 4749 4767 2199 152 4625 3585 1458 1065 668 4793 3510 497 686 1221 3504 703 4726 2313 2123 4234 1721 ))
 (push 2)
 (declare-fun v144 () Bool)
 (pop 12)
 (declare-fun S1-1 () S1)
 (declare-fun v145 () Bool)
 (declare-fun v146 () Bool)
 (declare-fun v147 () Bool)
 (declare-fun v148 () Bool)
 (declare-fun i54 () Int)
 (declare-fun v149 () Bool)
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i54 ) (2465 4255 4152 4210 4493 2874 494 2965 2408 3538 2850 4508 395 4064 4694 2821 3238 ))
 (declare-fun v150 () Bool)
 (declare-fun i55 () Int)
 (declare-fun v153 () Bool)
 (declare-fun v154 () Bool)
 (pop 1)
 (declare-fun v155 () Bool)
 (push 1)
 (declare-fun v157 () Bool)
 (declare-fun v158 () Bool)
 (push 2)
 (declare-fun v159 () Bool)
 (push 2)
 (declare-fun i56 () Int)
 (declare-fun i57 () Int)
 (check-sat-assuming-model (i3 i10) (2483 1464))
 (declare-fun v160 () Bool)
 (declare-fun v161 () Bool)
 (declare-fun i58 () Int)
 (pop 3)
 (declare-fun v162 () Bool)
 (declare-fun v163 () Bool)
 (declare-fun i59 () Int)
 (declare-fun v164 () Bool)
 (push 2)
 (declare-fun v165 () Bool)
 (declare-fun v166 () Bool)
 (declare-fun v167 () Bool)
 (declare-fun v168 () Bool)
 (declare-fun v169 () Bool)
 (declare-fun v170 () Bool)
 (pop 3)
 (declare-fun v171 () Bool)
 (declare-fun v172 () Bool)
 (declare-fun v173 () Bool)
 (push 1)
 (declare-fun v174 () Bool)
 (declare-fun v175 () Bool)
 (push 1)
 (declare-fun v176 () Bool)
 (declare-fun v177 () Bool)
 (declare-fun v178 () Bool)
 (declare-fun v179 () Bool)
 (declare-fun v180 () Bool)
 (pop 3)
 (push 4)
 (declare-fun v181 () Bool)
 (declare-fun v182 () Bool)
 (declare-fun i60 () Int)
 (declare-fun v183 () Bool)
 (declare-fun v184 () Bool)
 (declare-fun v185 () Bool)
 (declare-fun v186 () Bool)
 (declare-fun i61 () Int)
 (declare-fun v187 () Bool)
 (declare-fun v188 () Bool)
 (declare-fun v189 () Bool)
 (declare-fun i62 () Int)
 (declare-fun v190 () Bool)
 (declare-fun v191 () Bool)
 (push 2)
 (declare-fun v192 () Bool)
 (push 4)
 (declare-fun v193 () Bool)
 (pop 5)
 (declare-fun v194 () Bool)
 (declare-fun i63 () Int)
 (declare-fun v195 () Bool)
 (pop 5)
 (declare-fun v196 () Bool)
 (declare-fun v198 () Bool)
 (declare-sort S2 0)
 (declare-fun v199 () Bool)
 (declare-fun v201 () Bool)
 (push 4)
 (declare-fun v202 () Bool)
 (declare-fun v203 () Bool)
 (declare-fun v204 () Bool)
 (declare-fun v205 () Bool)
 (declare-fun i64 () Int)
 (declare-fun v206 () Bool)
 (declare-fun S2-0 () S2)
 (declare-fun v207 () Bool)
 (declare-fun i65 () Int)
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i64 i65 ) (2756 1080 3150 145 3513 913 1467 2866 4952 125 50 2121 543 4607 3563 4346 1146 3881 ))
 (declare-fun v208 () Bool)
 (declare-fun i66 () Int)
 (declare-fun i67 () Int)
 (declare-fun v210 () Bool)
 (declare-fun i68 () Int)
 (push 4)
 (declare-fun v211 () Bool)
 (declare-fun i69 () Int)
 (declare-fun v212 () Bool)
 (declare-fun v213 () Bool)
 (declare-fun i70 () Int)
 (declare-fun v214 () Bool)
 (declare-fun v215 () Bool)
 (declare-fun i71 () Int)
 (push 2)
 (declare-fun v216 () Bool)
 (declare-fun i72 () Int)
 (declare-fun v217 () Bool)
 (push 5)
 (declare-fun v221 () Bool)
 (declare-fun v222 () Bool)
 (declare-fun v223 () Bool)
 (declare-fun v224 () Bool)
 (declare-fun v225 () Bool)
 (declare-fun i74 () Int)
 (push 3)
 (declare-fun v226 () Bool)
 (pop 13)
 (declare-fun v227 () Bool)
 (declare-fun v228 () Bool)
 (push 3)
 (declare-fun v229 () Bool)
 (declare-fun v230 () Bool)
 (push 5)
 (declare-fun v231 () Bool)
 (push 4)
 (declare-fun v232 () Bool)
 (declare-fun v233 () Bool)
 (pop 15)
 (declare-fun v234 () Bool)
 (declare-fun S0-1 () S0)
 (declare-fun v235 () Bool)
 (declare-fun v236 () Bool)
 (declare-fun v237 () Bool)
 (declare-fun v238 () Bool)
 (declare-fun i75 () Int)
 (declare-fun v239 () Bool)
 (declare-fun i76 () Int)
 (declare-fun v240 () Bool)
 (pop 1)
 (declare-fun v242 () Bool)
 (declare-fun v246 () Bool)
 (push 1)
 (declare-fun v247 () Bool)
 (declare-fun v248 () Bool)
 (pop 1)
 (check-sat-assuming-model (i2 i16) (227 3631))
 (declare-sort S3 0)
 (push 2)
 (declare-fun v252 () Bool)
 (declare-fun v253 () Bool)
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 ) (1247 1307 10 368 4559 1164 1922 1205 578 2154 3940 4150 4572 3539 3666 325 ))
 (declare-fun v254 () Bool)
 (declare-fun v255 () Bool)
 (declare-fun v256 () Bool)
 (declare-fun v257 () Bool)
 (declare-fun v258 () Bool)
 (declare-fun v259 () Bool)
 (declare-fun v260 () Bool)
 (pop 2)
 (declare-fun v261 () Bool)
 (push 2)
 (declare-fun v263 () Bool)
 (push 4)
 (declare-fun v264 () Bool)
 (pop 6)
 (declare-fun v267 () Bool)
 (declare-fun v268 () Bool)
 (declare-fun v270 () Bool)
 (check-sat-assuming-model (i9 i17 i20) (1635 2075 25))
 (declare-fun v271 () Bool)
 (declare-fun i77 () Int)
 (declare-fun i78 () Int)
 (push 1)
 (declare-fun i79 () Int)
 (declare-fun v275 () Bool)
 (declare-fun v276 () Bool)
 (declare-fun v277 () Bool)
 (declare-fun i80 () Int)
 (declare-fun v278 () Bool)
 (pop 1)
 (declare-fun v279 () Bool)
 (declare-sort S4 0)
 (declare-fun i81 () Int)
 (declare-fun v281 () Bool)
 (declare-fun v285 () Bool)
 (push 4)
 (declare-fun v286 () Bool)
 (declare-fun v287 () Bool)
 (declare-fun v288 () Bool)
 (declare-fun v289 () Bool)
 (push 5)
 (declare-fun v290 () Bool)
 (declare-fun v291 () Bool)
 (declare-fun i82 () Int)
 (pop 4)
 (declare-fun v292 () Bool)
 (pop 5)
 (declare-fun S2-0 () S2)
 (declare-fun v293 () Bool)
 (check-sat-assuming-model (i9 i19) (2856 4535))
 (push 1)
 (declare-fun v295 () Bool)
 (declare-fun i83 () Int)
 (push 2)
 (declare-fun S3-0 () S3)
 (declare-fun v296 () Bool)
 (push 1)
 (declare-fun i84 () Int)
 (declare-fun v297 () Bool)
 (declare-fun v298 () Bool)
 (declare-fun v299 () Bool)
 (declare-fun v300 () Bool)
 (pop 3)
 (declare-fun i85 () Int)
 (declare-fun v301 () Bool)
 (declare-fun i86 () Int)
 (declare-fun v302 () Bool)
 (declare-fun i87 () Int)
 (pop 1)
 (declare-fun v303 () Bool)
 (check-sat-assuming-model (i8 i77 i78) (2950 2742 3299))
 (declare-fun v307 () Bool)
 (declare-fun v308 () Bool)
 (declare-fun v310 () Bool)
 (push 1)
 (declare-fun S3-0 () S3)
 (declare-fun v311 () Bool)
 (push 3)
 (declare-fun i88 () Int)
 (declare-fun v312 () Bool)
 (declare-fun v313 () Bool)
 (declare-fun i89 () Int)
 (declare-fun v314 () Bool)
 (declare-fun v315 () Bool)
 (pop 1)
 (declare-fun v316 () Bool)
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i77 i78 i81 ) (4857 2011 3785 3477 927 4871 1946 4150 2248 1394 903 915 2554 4609 311 4350 524 2380 3799 ))
 (declare-fun v317 () Bool)
 (pop 1)
 (declare-fun v318 () Bool)
 (declare-fun v319 () Bool)
 (declare-fun i90 () Int)
 (declare-fun v320 () Bool)
 (push 4)
 (declare-fun v321 () Bool)
 (pop 1)
 (declare-fun v322 () Bool)
 (pop 1)
 (declare-fun i91 () Int)
 (push 1)
 (declare-fun v323 () Bool)
 (declare-fun v324 () Bool)
 (declare-fun v325 () Bool)
 (declare-fun i92 () Int)
 (push 2)
 (declare-fun i93 () Int)
 (declare-fun v326 () Bool)
 (declare-fun v327 () Bool)
 (pop 1)
 (push 4)
 (declare-fun v328 () Bool)
 (declare-fun i94 () Int)
 (declare-fun v329 () Bool)
 (declare-fun v330 () Bool)
 (pop 5)
 (declare-fun v331 () Bool)
 (declare-fun v332 () Bool)
 (declare-fun i95 () Int)
 (declare-fun v333 () Bool)
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i77 i78 i81 i90 i91 i92 i95 ) (1480 1299 4448 1264 719 706 939 2648 792 3130 3306 2783 2712 152 4922 2635 4040 4215 1914 367 3444 2203 4078 ))
 (declare-fun S0-2 () S0)
 (push 1)
 (push 5)
 (declare-fun v334 () Bool)
 (pop 6)
 (declare-fun v335 () Bool)
 (push 2)
 (declare-fun v336 () Bool)
 (declare-fun i96 () Int)
 (declare-fun v337 () Bool)
 (push 4)
 (declare-fun v338 () Bool)
 (declare-fun i97 () Int)
 (push 2)
 (push 2)
 (declare-fun i98 () Int)
 (declare-fun v339 () Bool)
 (declare-fun i99 () Int)
 (pop 13)
 (declare-fun v340 () Bool)
 (push 3)
 (declare-fun v341 () Bool)
 (declare-fun S1-1 () S1)
 (declare-fun v342 () Bool)
 (push 3)
 (declare-fun v343 () Bool)
 (declare-fun v344 () Bool)
 (declare-fun i100 () Int)
 (declare-fun v345 () Bool)
 (declare-fun i101 () Int)
 (declare-fun v346 () Bool)
 (declare-fun S4-1 () S4)
 (declare-fun v347 () Bool)
 (declare-fun v348 () Bool)
 (declare-fun v349 () Bool)
 (declare-fun v350 () Bool)
 (declare-fun v351 () Bool)
 (pop 2)
 (declare-fun v352 () Bool)
 (declare-fun v353 () Bool)
 (declare-fun v354 () Bool)
 (declare-fun i102 () Int)
 (push 3)
 (declare-fun v355 () Bool)
 (pop 2)
 (declare-fun v356 () Bool)
 (declare-fun i103 () Int)
 (declare-fun v357 () Bool)
 (declare-fun v358 () Bool)
 (push 1)
 (declare-fun i104 () Int)
 (declare-fun i105 () Int)
 (declare-fun v359 () Bool)
 (push 2)
 (declare-fun v360 () Bool)
 (pop 5)
 (declare-fun i106 () Int)
 (declare-fun v361 () Bool)
 (pop 3)
 (declare-fun v362 () Bool)
 (declare-fun v363 () Bool)
 (declare-fun i107 () Int)
 (declare-fun v364 () Bool)
 (declare-fun i108 () Int)
 (declare-fun v365 () Bool)
 (push 1)
 (declare-fun i109 () Int)
 (declare-fun v366 () Bool)
 (declare-fun v367 () Bool)
 (push 1)
 (declare-fun v368 () Bool)
 (declare-fun v369 () Bool)
 (push 3)
 (declare-fun v370 () Bool)
 (push 5)
 (declare-fun v371 () Bool)
 (push 4)
 (declare-fun v372 () Bool)
 (pop 13)
 (declare-fun v373 () Bool)
 (pop 3)
 (declare-fun v374 () Bool)
 (push 5)
 (declare-fun v376 () Bool)
 (push 2)
 (declare-fun v377 () Bool)
 (declare-fun v378 () Bool)
 (declare-fun v379 () Bool)
 (declare-fun v380 () Bool)
 (declare-fun S0-2 () S0)
 (declare-fun v381 () Bool)
 (declare-fun i110 () Int)
 (declare-fun v382 () Bool)
 (declare-fun v383 () Bool)
 (declare-fun i111 () Int)
 (declare-fun v384 () Bool)
 (push 2)
 (declare-fun v385 () Bool)
 (pop 7)
 (declare-fun v386 () Bool)
 (declare-fun v387 () Bool)
 (declare-fun v388 () Bool)
 (pop 2)
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i77 i78 i81 ) (3818 1152 3610 2964 3791 2264 545 3534 4177 1607 4760 243 708 2206 2563 4316 4194 4080 4082 ))
 (declare-fun v392 () Bool)
 (declare-fun i112 () Int)
 (declare-fun v394 () Bool)
 (declare-fun v397 () Bool)
 (push 2)
 (declare-fun v402 () Bool)
 (pop 2)
 (declare-fun i113 () Int)
 (declare-fun v404 () Bool)
 (declare-fun i114 () Int)
 (declare-fun i115 () Int)
 (declare-fun i116 () Int)
 (declare-fun i117 () Int)
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i77 i78 i81 i112 i113 i114 i115 i116 i117 ) (3629 55 1482 3404 3870 821 1292 1988 1049 2572 2039 1252 4922 3515 3367 338 4609 1731 3662 2022 2698 4679 2376 2197 4948 ))
 (declare-fun v416 () Bool)
 (declare-fun i118 () Int)
 (declare-fun v420 () Bool)
 (declare-fun v421 () Bool)
 (push 3)
 (declare-fun S1-1 () S1)
 (declare-fun v423 () Bool)
 (declare-fun v424 () Bool)
 (declare-fun v425 () Bool)
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i77 i78 i81 i112 i113 i114 i115 i116 i117 i118 ) (150 3562 2190 3308 3643 2999 1137 512 967 317 4249 2952 4570 1515 4272 2093 4173 839 212 1726 1769 1324 3469 1865 2975 4964 ))
 (check-sat-assuming-model (i10 i17) (1812 2700))
 (declare-fun v426 () Bool)
 (declare-fun i119 () Int)
 (declare-fun v427 () Bool)
 (declare-fun v428 () Bool)
 (declare-fun v429 () Bool)
 (push 3)
 (declare-fun v430 () Bool)
 (declare-fun v431 () Bool)
 (declare-fun v432 () Bool)
 (declare-fun v433 () Bool)
 (declare-fun i120 () Int)
 (declare-fun v434 () Bool)
 (push 5)
 (declare-fun v435 () Bool)
 (declare-fun v436 () Bool)
 (declare-fun i121 () Int)
 (declare-fun i122 () Int)
 (declare-fun v437 () Bool)
 (push 3)
 (declare-fun v438 () Bool)
 (declare-fun v439 () Bool)
 (declare-fun v440 () Bool)
 (declare-fun v441 () Bool)
 (declare-fun v442 () Bool)
 (declare-fun v443 () Bool)
 (declare-fun v444 () Bool)
 (declare-fun v445 () Bool)
 (declare-fun i123 () Int)
 (declare-fun v446 () Bool)
 (pop 7)
 (declare-fun i124 () Int)
 (declare-fun v447 () Bool)
 (push 1)
 (push 2)
 (declare-fun v448 () Bool)
 (declare-fun v449 () Bool)
 (declare-fun v450 () Bool)
 (declare-fun v451 () Bool)
 (declare-fun v452 () Bool)
 (declare-fun i125 () Int)
 (declare-fun v453 () Bool)
 (declare-fun i126 () Int)
 (pop 6)
 (push 2)
 (declare-fun v454 () Bool)
 (declare-fun i127 () Int)
 (declare-fun v455 () Bool)
 (push 2)
 (declare-fun v456 () Bool)
 (declare-fun v457 () Bool)
 (declare-fun v458 () Bool)
 (declare-fun i128 () Int)
 (declare-fun v459 () Bool)
 (declare-fun i129 () Int)
 (declare-fun v460 () Bool)
 (pop 7)
 (declare-fun i130 () Int)
 (declare-fun v461 () Bool)
 (declare-fun i131 () Int)
 (declare-fun v462 () Bool)
 (declare-fun v463 () Bool)
 (declare-fun v464 () Bool)
 (declare-fun v465 () Bool)
 (declare-fun v466 () Bool)
 (declare-fun v467 () Bool)
 (pop 1)
 (declare-fun i132 () Int)
 (push 5)
 (declare-fun v470 () Bool)
 (declare-fun v471 () Bool)
 (declare-fun v472 () Bool)
 (declare-fun v473 () Bool)
 (declare-fun i133 () Int)
 (declare-fun v474 () Bool)
 (declare-fun v475 () Bool)
 (declare-fun v476 () Bool)
 (declare-fun v477 () Bool)
 (declare-fun v478 () Bool)
 (declare-fun i134 () Int)
 (declare-fun v479 () Bool)
 (declare-fun v480 () Bool)
 (declare-fun i135 () Int)
 (declare-fun v481 () Bool)
 (declare-fun v482 () Bool)
 (declare-fun S4-2 () S4)
 (declare-fun v483 () Bool)
 (declare-fun v484 () Bool)
 (declare-fun v485 () Bool)
 (declare-fun v486 () Bool)
 (declare-fun i136 () Int)
 (declare-fun v487 () Bool)
 (declare-fun i137 () Int)
 (declare-fun v488 () Bool)
 (declare-fun v489 () Bool)
 (declare-fun v490 () Bool)
 (declare-fun v491 () Bool)
 (declare-fun v492 () Bool)
 (declare-fun v493 () Bool)
 (declare-fun v494 () Bool)
 (declare-fun v495 () Bool)
 (declare-fun i138 () Int)
 (declare-fun v496 () Bool)
 (declare-fun v497 () Bool)
 (pop 1)
 (declare-fun i139 () Int)
 (declare-fun v499 () Bool)
 (push 4)
 (declare-fun v500 () Bool)
 (declare-fun i140 () Int)
 (declare-fun v501 () Bool)
 (declare-fun v502 () Bool)
 (declare-fun v503 () Bool)
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i77 i78 i81 i112 i113 i114 i115 i116 i117 i118 i132 i139 ) (1086 2966 91 2582 3716 3066 2757 1849 1791 3936 487 2225 3704 608 812 137 2893 4715 1972 5000 2826 31 2607 2316 1151 504 4763 736 ))
 (declare-fun v504 () Bool)
 (declare-fun v505 () Bool)
 (declare-fun v506 () Bool)
 (declare-fun v507 () Bool)
 (declare-fun v508 () Bool)
 (declare-fun i141 () Int)
 (declare-fun v509 () Bool)
 (declare-fun v510 () Bool)
 (pop 2)
 (declare-fun i142 () Int)
 (push 3)
 (declare-fun v512 () Bool)
 (declare-fun S4-2 () S4)
 (declare-fun v513 () Bool)
 (declare-fun v514 () Bool)
 (declare-fun v515 () Bool)
 (declare-fun v516 () Bool)
 (declare-fun v517 () Bool)
 (push 4)
 (declare-fun v518 () Bool)
 (declare-fun v519 () Bool)
 (declare-fun S1-1 () S1)
 (declare-fun i143 () Int)
 (declare-fun v520 () Bool)
 (declare-fun i144 () Int)
 (declare-fun v521 () Bool)
 (declare-fun v522 () Bool)
 (declare-fun v523 () Bool)
 (declare-fun v524 () Bool)
 (declare-fun v525 () Bool)
 (declare-fun v526 () Bool)
 (declare-fun v527 () Bool)
 (declare-fun v528 () Bool)
 (declare-fun v529 () Bool)
 (declare-fun i145 () Int)
 (declare-fun v530 () Bool)
 (declare-fun v531 () Bool)
 (declare-fun S3-0 () S3)
 (declare-fun v532 () Bool)
 (declare-fun v533 () Bool)
 (declare-fun i146 () Int)
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i77 i78 i81 i112 i113 i114 i115 i116 i117 i118 i132 i139 i142 i143 i144 i145 i146 ) (4277 2718 2794 841 4112 634 4559 207 1201 2959 4373 1231 2454 25 4326 396 3592 3154 517 4061 3560 2912 4102 4476 226 841 2786 918 3603 3615 2530 4429 3387 ))
 (push 3)
 (declare-fun v534 () Bool)
 (declare-fun v535 () Bool)
 (declare-fun v536 () Bool)
 (declare-fun v537 () Bool)
 (pop 3)
 (declare-fun v538 () Bool)
 (declare-fun v539 () Bool)
 (declare-fun v540 () Bool)
 (declare-fun v541 () Bool)
 (push 3)
 (declare-fun v542 () Bool)
 (declare-fun v543 () Bool)
 (declare-fun i147 () Int)
 (pop 4)
 (declare-fun v544 () Bool)
 (declare-fun v545 () Bool)
 (check-sat-assuming-model (i17 i23 i142) (1212 4422 1911))
 (declare-fun v546 () Bool)
 (declare-fun i148 () Int)
 (declare-fun v547 () Bool)
 (declare-fun v548 () Bool)
 (declare-fun v549 () Bool)
 (pop 3)
 (declare-fun v552 () Bool)
 (declare-fun i149 () Int)
 (declare-fun v553 () Bool)
 (declare-fun v554 () Bool)
 (declare-fun v555 () Bool)
 (declare-fun i150 () Int)
 (declare-fun v556 () Bool)
 (declare-fun v557 () Bool)
 (declare-fun v558 () Bool)
 (pop 1)
 (declare-fun v559 () Bool)
 (declare-fun i151 () Int)
 (push 4)
 (declare-fun v560 () Bool)
 (declare-fun v561 () Bool)
 (declare-fun v562 () Bool)
 (declare-fun v563 () Bool)
 (declare-fun v564 () Bool)
 (declare-fun v565 () Bool)
 (push 5)
 (declare-fun v566 () Bool)
 (declare-fun v567 () Bool)
 (check-sat-assuming-model (i0 i2 i114) (4462 4904 803))
 (declare-fun v568 () Bool)
 (push 4)
 (declare-fun v569 () Bool)
 (declare-fun v570 () Bool)
 (declare-fun v571 () Bool)
 (declare-fun v572 () Bool)
 (declare-fun v573 () Bool)
 (declare-fun i152 () Int)
 (pop 9)
 (declare-fun v574 () Bool)
 (push 5)
 (declare-fun v575 () Bool)
 (declare-fun i153 () Int)
 (declare-fun i154 () Int)
 (declare-fun v576 () Bool)
 (declare-fun i155 () Int)
 (declare-fun v577 () Bool)
 (check-sat-assuming-model (i1 i2 i117) (1429 1371 615))
 (pop 5)
 (declare-fun v578 () Bool)
 (declare-fun v579 () Bool)
 (declare-fun v580 () Bool)
 (push 5)
 (declare-fun i156 () Int)
 (declare-fun v581 () Bool)
 (declare-fun v582 () Bool)
 (declare-fun v583 () Bool)
 (declare-fun v584 () Bool)
 (declare-fun i157 () Int)
 (declare-fun v585 () Bool)
 (declare-fun v586 () Bool)
 (declare-fun i158 () Int)
 (declare-fun v587 () Bool)
 (declare-fun v588 () Bool)
 (push 2)
 (declare-fun v589 () Bool)
 (pop 11)
 (declare-fun i159 () Int)
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i77 i78 i81 i112 i113 i114 i115 i116 i117 i118 i132 i139 i142 i151 i159 ) (855 4057 907 1663 3930 1359 4239 4393 3541 1755 286 1911 2770 3663 1746 4205 3101 2548 2817 2491 2492 3064 1084 4542 2298 3879 943 2490 1802 4310 1524 ))
 (declare-fun i160 () Int)
 (declare-fun v593 () Bool)
 (push 4)
 (declare-fun v594 () Bool)
 (declare-fun i161 () Int)
 (declare-fun v595 () Bool)
 (pop 4)
 (declare-fun v598 () Bool)
 (declare-fun v599 () Bool)
 (push 4)
 (declare-fun v602 () Bool)
 (declare-fun v603 () Bool)
 (declare-fun i162 () Int)
 (push 4)
 (declare-fun v604 () Bool)
 (declare-fun v605 () Bool)
 (declare-fun i163 () Int)
 (declare-fun v606 () Bool)
 (declare-fun v607 () Bool)
 (declare-fun v608 () Bool)
 (declare-fun v609 () Bool)
 (push 3)
 (declare-fun v610 () Bool)
 (declare-fun v611 () Bool)
 (push 2)
 (declare-fun v612 () Bool)
 (declare-fun i164 () Int)
 (pop 9)
 (declare-fun v613 () Bool)
 (pop 3)
 (push 2)
 (declare-fun v617 () Bool)
 (declare-fun v618 () Bool)
 (pop 2)
 (declare-fun v619 () Bool)
 (declare-fun i165 () Int)
 (declare-fun i166 () Int)
 (declare-fun i167 () Int)
 (declare-fun i168 () Int)
 (declare-fun i169 () Int)
 (declare-fun i170 () Int)
 (declare-fun i171 () Int)
 (declare-fun i172 () Int)
 (declare-fun i173 () Int)
 (push 4)
 (declare-fun S2-1 () S2)
 (declare-fun v640 () Bool)
 (declare-fun v641 () Bool)
 (declare-fun v642 () Bool)
 (declare-fun v643 () Bool)
 (declare-fun v644 () Bool)
 (declare-fun i174 () Int)
 (declare-fun v645 () Bool)
 (declare-fun v646 () Bool)
 (declare-fun v647 () Bool)
 (declare-fun v648 () Bool)
 (declare-fun i175 () Int)
 (push 2)
 (declare-fun v649 () Bool)
 (push 4)
 (declare-fun v650 () Bool)
 (declare-fun v651 () Bool)
 (declare-fun v652 () Bool)
 (push 3)
 (declare-fun v653 () Bool)
 (declare-fun v654 () Bool)
 (pop 12)
 (declare-fun v655 () Bool)
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i77 i78 i81 i112 i113 i114 i115 i116 i117 i118 i132 i139 i142 i151 i159 i160 i165 i166 i167 i168 i169 i170 i171 i172 i173 ) (3612 505 2315 1866 2918 1615 4894 3447 1686 3279 2051 1528 146 4901 2016 2259 2931 249 4484 2654 391 2960 174 2427 4545 4348 1740 2328 3841 4363 1597 2073 2193 89 898 1605 2795 4996 2380 599 2564 ))
 (declare-fun i176 () Int)
 (declare-fun v656 () Bool)
 (declare-fun v657 () Bool)
 (pop 1)
 (push 5)
 (declare-fun v658 () Bool)
 (declare-fun v659 () Bool)
 (declare-fun v660 () Bool)
 (declare-fun v661 () Bool)
 (declare-fun v662 () Bool)
 (declare-fun v663 () Bool)
 (declare-fun i177 () Int)
 (push 3)
 (declare-fun v664 () Bool)
 (declare-fun i178 () Int)
 (declare-fun v665 () Bool)
 (declare-fun v666 () Bool)
 (declare-fun v667 () Bool)
 (declare-fun v668 () Bool)
 (declare-fun v669 () Bool)
 (declare-fun v670 () Bool)
 (declare-fun v671 () Bool)
 (declare-fun v672 () Bool)
 (assert (uf4 (distinct S2-0 S2-0 S2-0 S2-0) v9 v421 (= 878 i15)))
 (push 3)
 (declare-fun v673 () Bool)
 (declare-fun v674 () Bool)
 (declare-fun v675 () Bool)
 (declare-fun i179 () Int)
 (declare-fun v676 () Bool)
 (declare-fun v677 () Bool)
 (declare-fun v678 () Bool)
 (declare-fun v679 () Bool)
 (declare-fun i180 () Int)
 (declare-fun v680 () Bool)
 (declare-fun v681 () Bool)
 (declare-fun v682 () Bool)
 (push 3)
 (declare-fun v683 () Bool)
 (declare-fun v684 () Bool)
 (declare-fun v685 () Bool)
 (declare-fun v686 () Bool)
 (declare-fun v687 () Bool)
 (declare-fun i181 () Int)
 (declare-fun v688 () Bool)
 (pop 13)
 (declare-fun v689 () Bool)
 (declare-fun i182 () Int)
 (declare-fun v690 () Bool)
 (pop 1)
 (declare-fun v691 () Bool)
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i77 i78 i81 i112 i113 i114 i115 i116 i117 i118 i132 i139 i142 i151 i159 i160 i165 i166 i167 i168 i169 i170 i171 i172 i173 ) (952 916 4600 1715 2384 3807 1969 1457 3767 2721 3796 96 604 1532 112 4023 3569 620 2092 3222 3733 2087 2737 1219 3299 442 4544 1960 3420 2402 643 2697 3061 2851 4891 635 95 1992 857 1719 2275 ))
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i77 i78 i81 i112 i113 i114 i115 i116 i117 i118 i132 i139 i142 i151 i159 i160 i165 i166 i167 i168 i169 i170 i171 i172 i173 ) (2082 4497 4117 70 3330 1182 4787 3395 753 3154 2584 3520 1407 1392 3932 1765 546 3061 3935 465 4517 3549 4338 518 538 2945 791 1703 1422 890 3353 2048 1171 2435 4767 3410 72 1059 46 4806 3259 ))
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i77 i78 i81 i112 i113 i114 i115 i116 i117 i118 i132 i139 i142 i151 i159 i160 i165 i166 i167 i168 i169 i170 i171 i172 i173 ) (4360 3680 4078 1906 2290 4748 4374 4478 4397 155 4807 2892 1480 2920 3390 305 3316 687 3061 721 1008 3915 4330 1807 1852 62 4391 1351 2541 3007 3444 2414 1449 971 3221 2326 3229 4295 519 3882 4118 ))
 (push 4)
 (declare-fun S0-2 () S0)
 (declare-fun v692 () Bool)
 (declare-fun S2-1 () S2)
 (declare-fun v693 () Bool)
 (declare-fun v694 () Bool)
 (declare-fun v695 () Bool)
 (pop 1)
 (declare-fun v696 () Bool)
 (declare-fun v697 () Bool)
 (declare-fun v698 () Bool)
 (declare-fun v699 () Bool)
 (declare-fun v700 () Bool)
 (declare-fun i183 () Int)
 (declare-fun S2-1 () S2)
 (declare-fun v701 () Bool)
 (declare-fun v702 () Bool)
 (declare-fun v703 () Bool)
 (declare-fun i184 () Int)
 (declare-fun v704 () Bool)
 (pop 3)
 (push 2)
 (declare-fun v705 () Bool)
 (declare-fun v706 () Bool)
 (declare-fun v707 () Bool)
 (declare-fun i185 () Int)
 (declare-fun v708 () Bool)
 (declare-fun v709 () Bool)
 (declare-fun i186 () Int)
 (push 3)
 (declare-fun v710 () Bool)
 (pop 2)
 (declare-fun v711 () Bool)
 (declare-fun v712 () Bool)
 (declare-fun S0-2 () S0)
 (push 2)
 (declare-fun v713 () Bool)
 (declare-fun v714 () Bool)
 (declare-fun v715 () Bool)
 (declare-fun v716 () Bool)
 (declare-fun v717 () Bool)
 (declare-fun i187 () Int)
 (push 4)
 (declare-fun v718 () Bool)
 (declare-fun v719 () Bool)
 (declare-fun v720 () Bool)
 (declare-fun v721 () Bool)
 (declare-fun i188 () Int)
 (declare-fun v722 () Bool)
 (declare-fun i189 () Int)
 (pop 4)
 (declare-fun v723 () Bool)
 (declare-fun v724 () Bool)
 (declare-fun v725 () Bool)
 (push 2)
 (declare-fun v726 () Bool)
 (declare-fun v727 () Bool)
 (declare-fun v728 () Bool)
 (declare-fun v729 () Bool)
 (declare-fun v730 () Bool)
 (push 5)
 (declare-fun v731 () Bool)
 (declare-fun v732 () Bool)
 (declare-fun v733 () Bool)
 (declare-fun v734 () Bool)
 (declare-fun v735 () Bool)
 (declare-fun v736 () Bool)
 (declare-fun v737 () Bool)
 (declare-fun v738 () Bool)
 (push 4)
 (declare-fun v739 () Bool)
 (pop 5)
 (declare-fun v740 () Bool)
 (declare-fun v741 () Bool)
 (declare-fun v742 () Bool)
 (push 3)
 (declare-fun v743 () Bool)
 (declare-fun v744 () Bool)
 (declare-fun i190 () Int)
 (declare-fun i191 () Int)
 (declare-fun v745 () Bool)
 (declare-fun v746 () Bool)
 (declare-fun v747 () Bool)
 (declare-fun v748 () Bool)
 (declare-fun v749 () Bool)
 (pop 14)
 (declare-fun i192 () Int)
 (push 3)
 (declare-fun v751 () Bool)
 (push 4)
 (declare-fun i193 () Int)
 (declare-fun v752 () Bool)
 (declare-fun v753 () Bool)
 (pop 7)
 (push 1)
 (declare-fun i194 () Int)
 (declare-fun v756 () Bool)
 (declare-fun v757 () Bool)
 (pop 1)
 (declare-fun i195 () Int)
 (push 2)
 (declare-fun v759 () Bool)
 (push 5)
 (declare-fun v760 () Bool)
 (push 1)
 (declare-fun i196 () Int)
 (pop 8)
 (push 3)
 (declare-fun v761 () Bool)
 (declare-fun i197 () Int)
 (declare-fun v762 () Bool)
 (declare-fun v763 () Bool)
 (declare-fun v764 () Bool)
 (declare-fun v765 () Bool)
 (declare-fun v766 () Bool)
 (declare-fun v767 () Bool)
 (push 4)
 (assert (xor (= (>= 295 418) v394 (distinct v310 (or v46 v29 (> i10 (ufbi3 v2 v0 v7) (+ 53 49 i7 i7 230) 90 406 292) v6) (> (mod i5 810) i5 i7 i3 i8 i2) (> i19 i16) v34 (> i1 (+ 53 49 i7 i7 230) (- 370 90) 53 53 408) v242) (distinct (and v7 v8) (uf3 (= 230 90) (< i17 (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7)) i9 (- 370 90) i19 49) v9) (= (+ 49 i3) (abs 406))) (xor v11 v261 (xor v2 (= v3 v1 v10 v1 v6 v10 v3) v0) (< (mod i5 810) i16) v28)) (= (abs 370) i1 (ufbi7 (=> (or (> i7 (- i9 i10) i1 i2) (not v0)) (distinct 370 (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7)))) v57 (not v45) (uf4 (< (mod i5 810) i16) (not v0) (> (mod i5 810) i5 i7 i3 i8 i2) (or (and v7 v8) v29 v7 (distinct (and v7 v8) v5) v2 (< (mod i5 810) (div i5 816)) (> (mod i5 810) i5 i7 i3 i8 i2))) v7 (> i19 i16) (distinct (+ i16 i5) i1)) 66) v691 v307 v420 (or (or v1 v1 v5 v0) v6 v6 v2 v0 v9)))
 (declare-fun v768 () Bool)
 (declare-fun i198 () Int)
 (pop 5)
 (declare-fun v769 () Bool)
 (declare-fun i199 () Int)
 (declare-fun v770 () Bool)
 (declare-fun v771 () Bool)
 (declare-fun v772 () Bool)
 (push 2)
 (declare-fun v773 () Bool)
 (declare-fun v774 () Bool)
 (declare-fun i200 () Int)
 (push 1)
 (pop 3)
 (declare-fun v775 () Bool)
 (declare-fun v776 () Bool)
 (declare-fun v777 () Bool)
 (push 4)
 (declare-fun v778 () Bool)
 (push 2)
 (declare-fun v779 () Bool)
 (declare-fun v780 () Bool)
 (declare-fun i201 () Int)
 (declare-fun v781 () Bool)
 (declare-fun v782 () Bool)
 (push 2)
 (declare-fun v783 () Bool)
 (declare-fun i202 () Int)
 (declare-fun v784 () Bool)
 (declare-fun i203 () Int)
 (push 1)
 (push 4)
 (declare-fun v785 () Bool)
 (declare-fun v786 () Bool)
 (pop 13)
 (declare-fun v787 () Bool)
 (push 2)
 (declare-fun v788 () Bool)
 (declare-fun v789 () Bool)
 (declare-fun v790 () Bool)
 (declare-fun v791 () Bool)
 (declare-fun i204 () Int)
 (pop 2)
 (declare-fun v792 () Bool)
 (push 3)
 (declare-fun v793 () Bool)
 (pop 5)
 (declare-fun i205 () Int)
 (check-sat-assuming-model (i9 i160 i171) (2167 1039 840))
 (push 3)
 (declare-fun v800 () Bool)
 (declare-fun i206 () Int)
 (push 1)
 (declare-fun v801 () Bool)
 (pop 4)
 (push 5)
 (declare-fun i207 () Int)
 (declare-fun v802 () Bool)
 (push 2)
 (declare-fun v803 () Bool)
 (declare-fun v804 () Bool)
 (declare-fun v805 () Bool)
 (declare-fun i208 () Int)
 (declare-fun v806 () Bool)
 (declare-fun v807 () Bool)
 (declare-fun v808 () Bool)
 (declare-fun v809 () Bool)
 (declare-fun v810 () Bool)
 (declare-fun S2-1 () S2)
 (push 3)
 (declare-fun v811 () Bool)
 (declare-fun i209 () Int)
 (pop 7)
 (declare-fun v812 () Bool)
 (declare-fun i210 () Int)
 (declare-fun v813 () Bool)
 (declare-fun v814 () Bool)
 (declare-fun v815 () Bool)
 (declare-fun i211 () Int)
 (declare-fun v816 () Bool)
 (declare-fun v817 () Bool)
 (declare-fun v818 () Bool)
 (declare-fun v819 () Bool)
 (declare-fun v820 () Bool)
 (push 4)
 (declare-fun v821 () Bool)
 (declare-fun v822 () Bool)
 (push 4)
 (declare-fun v823 () Bool)
 (declare-fun i212 () Int)
 (push 2)
 (declare-fun i213 () Int)
 (declare-fun v824 () Bool)
 (declare-fun i214 () Int)
 (declare-fun v825 () Bool)
 (declare-fun v826 () Bool)
 (declare-fun v827 () Bool)
 (declare-fun v828 () Bool)
 (assert (=> v155 (uf4 v268 (distinct (+ 53 49 i7 i7 230) (abs i5)) (xor (and (uf4 (< (+ i16 i5) 406 (- (- (div i5 816) 53 (+ 49 i3)) (- (div i5 816) 53 (+ 49 i3))) (ufbi3 v2 v0 v7) (div i7 882) (- (+ i5 53 (div i5 816)) i9 i2 53 230)) v242 v268 (=> v53 v31)) (not (or (not (>= 292 230)) (< (+ i16 i5) 406 (- (- (div i5 816) 53 (+ 49 i3)) (- (div i5 816) 53 (+ 49 i3))) (ufbi3 v2 v0 v7) (div i7 882) (- (+ i5 53 (div i5 816)) i9 i2 53 230))))) (uf4 (< (mod i5 810) i16) (not v0) (> (mod i5 810) i5 i7 i3 i8 i2) (or (and v7 v8) v29 v7 (distinct (and v7 v8) v5) v2 (< (mod i5 810) (div i5 816)) (> (mod i5 810) i5 i7 i3 i8 i2))) v8 v246 (distinct S0-0 S0-0 S0-0 S0-0 S0-0)) v281)))
 (declare-fun v829 () Bool)
 (declare-fun v830 () Bool)
 (declare-fun i215 () Int)
 (push 1)
 (declare-fun v831 () Bool)
 (declare-fun v832 () Bool)
 (declare-fun v833 () Bool)
 (declare-fun v834 () Bool)
 (declare-fun v835 () Bool)
 (declare-fun S3-0 () S3)
 (declare-fun v836 () Bool)
 (declare-fun v837 () Bool)
 (push 5)
 (declare-fun v838 () Bool)
 (push 1)
 (declare-fun v839 () Bool)
 (declare-fun v840 () Bool)
 (push 1)
 (declare-fun v841 () Bool)
 (pop 20)
 (declare-fun v842 () Bool)
 (declare-fun v843 () Bool)
 (declare-fun i216 () Int)
 (declare-fun i217 () Int)
 (declare-fun v844 () Bool)
 (declare-fun v845 () Bool)
 (declare-fun v846 () Bool)
 (declare-fun v847 () Bool)
 (pop 1)
 (declare-fun S1-1 () S1)
 (declare-fun i218 () Int)
 (declare-fun i219 () Int)
 (declare-fun i220 () Int)
 (assert (= v421 (distinct 716 161) (= (- 400 694) (* i2 992))))
 (declare-fun i221 () Int)
 (declare-fun i222 () Int)
 (push 1)
 (declare-fun v859 () Bool)
 (push 4)
 (declare-fun v860 () Bool)
 (declare-fun i223 () Int)
 (declare-fun v861 () Bool)
 (push 1)
 (declare-fun v862 () Bool)
 (declare-fun v863 () Bool)
 (pop 3)
 (declare-fun v864 () Bool)
 (pop 3)
 (push 5)
 (declare-fun v865 () Bool)
 (declare-fun v866 () Bool)
 (declare-fun v867 () Bool)
 (declare-fun v868 () Bool)
 (declare-fun i224 () Int)
 (declare-fun v869 () Bool)
 (declare-fun v870 () Bool)
 (declare-fun v871 () Bool)
 (push 3)
 (declare-fun v872 () Bool)
 (declare-fun i225 () Int)
 (declare-fun v873 () Bool)
 (declare-fun i226 () Int)
 (declare-fun v874 () Bool)
 (push 5)
 (declare-fun v875 () Bool)
 (declare-fun v876 () Bool)
 (declare-fun v877 () Bool)
 (declare-fun i227 () Int)
 (declare-fun v878 () Bool)
 (declare-fun v879 () Bool)
 (pop 4)
 (declare-fun v880 () Bool)
 (push 4)
 (declare-fun v881 () Bool)
 (declare-fun v882 () Bool)
 (declare-fun v883 () Bool)
 (declare-fun v884 () Bool)
 (declare-fun i228 () Int)
 (declare-fun v885 () Bool)
 (declare-fun v886 () Bool)
 (declare-fun v887 () Bool)
 (declare-fun v888 () Bool)
 (pop 11)
 (declare-fun i229 () Int)
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i77 i78 i81 i112 i113 i114 i115 i116 i117 i118 i132 i139 i142 i151 i159 i160 i165 i166 i167 i168 i169 i170 i171 i172 i173 i192 i195 i205 i218 i219 i220 i221 i222 i229 ) (1874 2640 2684 3923 4983 4551 2929 1610 2755 1743 2929 2377 1060 4736 2508 1370 3992 336 791 3005 889 1073 2255 3933 307 4571 3944 4146 575 4007 1949 4022 90 4719 4443 4475 3167 1409 3702 1052 2550 3083 2332 467 4118 1729 1642 2118 2353 2453 ))
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i77 i78 i81 i112 i113 i114 i115 i116 i117 i118 i132 i139 i142 i151 i159 i160 i165 i166 i167 i168 i169 i170 i171 i172 i173 i192 i195 i205 i218 i219 i220 i221 i222 i229 ) (4480 3736 3701 270 2685 2239 2175 2514 2101 4305 1777 4729 4010 1545 654 1591 304 143 2947 4811 1753 274 2314 4981 2362 965 1906 314 4413 3760 786 3203 1551 461 2118 3058 3411 2529 2760 4051 918 1589 1740 3259 301 4037 3308 1934 4985 3018 ))
 (declare-fun i230 () Int)
 (declare-fun v898 () Bool)
 (declare-fun i231 () Int)
 (push 5)
 (declare-fun v904 () Bool)
 (push 5)
 (declare-fun v905 () Bool)
 (declare-fun v906 () Bool)
 (declare-fun v907 () Bool)
 (declare-fun v908 () Bool)
 (declare-fun v909 () Bool)
 (declare-fun i232 () Int)
 (declare-fun v910 () Bool)
 (pop 6)
 (declare-fun v911 () Bool)
 (declare-fun v912 () Bool)
 (declare-fun v913 () Bool)
 (declare-fun i233 () Int)
 (declare-fun v914 () Bool)
 (declare-fun v915 () Bool)
 (declare-fun v916 () Bool)
 (declare-fun v917 () Bool)
 (declare-fun v918 () Bool)
 (declare-fun S2-2 () S2)
 (declare-fun v919 () Bool)
 (declare-fun v920 () Bool)
 (declare-fun i234 () Int)
 (push 4)
 (declare-fun v921 () Bool)
 (declare-fun v922 () Bool)
 (pop 3)
 (declare-fun v923 () Bool)
 (check-sat-assuming-model (i2 i171 i192) (268 2795 2370))
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i77 i78 i81 i112 i113 i114 i115 i116 i117 i118 i132 i139 i142 i151 i159 i160 i165 i166 i167 i168 i169 i170 i171 i172 i173 i192 i195 i205 i218 i219 i220 i221 i222 i229 i230 i231 i234 ) (4414 4005 4947 3669 3288 1133 1850 4296 1115 3029 3930 4515 3424 1559 23 4751 1827 2642 1925 876 835 4309 2657 4913 1541 2321 2998 323 267 4563 1748 3986 4479 3623 634 2098 3982 2292 1921 769 4865 1539 1338 1144 127 2599 3172 2987 2797 4290 1207 644 3778 ))
 (pop 1)
 (declare-fun S3-0 () S3)
 (declare-fun v924 () Bool)
 (declare-fun v925 () Bool)
 (pop 1)
 (declare-fun i235 () Int)
 (declare-fun i236 () Int)
 (declare-fun i237 () Int)
 (push 3)
 (declare-fun v930 () Bool)
 (declare-fun v931 () Bool)
 (declare-fun v932 () Bool)
 (push 2)
 (declare-fun v933 () Bool)
 (declare-fun i238 () Int)
 (check-sat-assuming-model (i159 i235) (1621 1134))
 (declare-fun v934 () Bool)
 (declare-fun v935 () Bool)
 (declare-fun i239 () Int)
 (declare-fun v936 () Bool)
 (declare-fun i240 () Int)
 (declare-fun i241 () Int)
 (declare-fun v937 () Bool)
 (assert (uf4_2 (or v308 (uf3 v52 (=> v392 (>= (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7)) 851)) v43) v201 v1 (distinct S1-1 S1-0 S1-1 S1-1) (= 390 (* (abs i8) 931)) (= v303 (and (not v45) (> (div i5 816) 772) (or v9 v2 v10 (= v3 v1 v10 v1 v6 v10 v3) v3 v6)) (<= (mod i5 810) 370) (or v29 v3 (=> v34 v5)) (> (mod i5 810) 897))) (<= 757 i116 (div 90 158) 636 i20 i20) (=> v47 v35) (xor (distinct 370 (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7))) (> (mod i5 810) 897))))
 (declare-fun v938 () Bool)
 (declare-fun i242 () Int)
 (assert (or v593 (not v404) (ufib3 (abs 406) 370 (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7)))))
 (declare-fun v939 () Bool)
 (declare-fun v940 () Bool)
 (pop 5)
 (declare-fun i243 () Int)
 (assert (and (and (= 341 408 (- 851) (abs i5) i151 i142) (distinct S1-0 S1-0) (xor v416 (xor (not v0) (=> v271 v268) (uf4 (< (mod i5 810) i16) (not v0) (> (mod i5 810) i5 i7 i3 i8 i2) (or (and v7 v8) v29 v7 (distinct (and v7 v8) v5) v2 (< (mod i5 810) (div i5 816)) (> (mod i5 810) i5 i7 i3 i8 i2))) v242 (= (and (distinct v44 v35 (= v44 (and v2 v32 v29 (xor v7 v7) v45 (or v31 v6 (> i7 (- i9 i10) i1 i2) v8 (and v7 v8) v7 v28) v5) (distinct 333 53) v31 (< (mod i5 810) i16) (= i2 (- 370 90))) (> i1 (+ 53 49 i7 i7 230) (- 370 90) 53 53 408) v35 (distinct 370 (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7))) (and v2 v32 v29 (xor v7 v7) v45 (or v31 v6 (> i7 (- i9 i10) i1 i2) v8 (and v7 v8) v7 v28) v5)) (distinct v44 v35 (= v44 (and v2 v32 v29 (xor v7 v7) v45 (or v31 v6 (> i7 (- i9 i10) i1 i2) v8 (and v7 v8) v7 v28) v5) (distinct 333 53) v31 (< (mod i5 810) i16) (= i2 (- 370 90))) (> i1 (+ 53 49 i7 i7 230) (- 370 90) 53 53 408) v35 (distinct 370 (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7))) (and v2 v32 v29 (xor v7 v7) v45 (or v31 v6 (> i7 (- i9 i10) i1 i2) v8 (and v7 v8) v7 v28) v5)) (=> v47 v35) (distinct v2 v5 (distinct 406 i16 i3 49 i17 408))) (< i17 (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7)) i9 (- 370 90) i19 49) (<= 897 (- (div i5 816) 53 (+ 49 i3)) 53 49) v6 (= 49 i7)) v242) (>= 295 220) (xor v7 v7) v619)) (=> (=> (distinct v2 v5 (distinct 406 i16 i3 49 i17 408)) v199) v198) (and (or (and (or v46 v29 (> i10 (ufbi3 v2 v0 v7) (+ 53 49 i7 i7 230) 90 406 292) v6) (= (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7)) 408) v307 (xor (> (mod i5 810) 897) (distinct v2 v5 (distinct 406 i16 i3 49 i17 408)) v46 (< 897 (- (+ i5 53 (div i5 816)) i9 i2 53 230)) (and v2 v32 v29 (xor v7 v7) v45 (or v31 v6 (> i7 (- i9 i10) i1 i2) v8 (and v7 v8) v7 v28) v5)) (xor (distinct (= i2 (- 370 90)) v59 (< i17 (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7)) i9 (- 370 90) i19 49) (< i17 (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7)) i9 (- 370 90) i19 49) (or v31 v6 (> i7 (- i9 i10) i1 i2) v8 (and v7 v8) v7 v28) (xor v2 (= v3 v1 v10 v1 v6 v10 v3) v0)) v45 (distinct 333 53) (= 49 i7) v2 (= (+ 49 i3) (abs 406))) (= (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7)) 408) (distinct v44 v35 (= v44 (and v2 v32 v29 (xor v7 v7) v45 (or v31 v6 (> i7 (- i9 i10) i1 i2) v8 (and v7 v8) v7 v28) v5) (distinct 333 53) v31 (< (mod i5 810) i16) (= i2 (- 370 90))) (> i1 (+ 53 49 i7 i7 230) (- 370 90) 53 53 408) v35 (distinct 370 (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7))) (and v2 v32 v29 (xor v7 v7) v45 (or v31 v6 (> i7 (- i9 i10) i1 i2) v8 (and v7 v8) v7 v28) v5))) (or (= (+ i16 i5) (* i2 992)) (=> v57 (<= (+ 53 49 i7 i7 230) (ufbi3 v2 v0 v7))) (distinct (distinct 333 53) v270 (> (- i3) (- 684 i5 161)) (< (mod i5 810) (div i5 816)) (or (distinct (+ i16 i5) i1) (not (or v31 v6 (> i7 (- i9 i10) i1 i2) v8 (and v7 v8) v7 v28)) v271)) (>= 88 (abs (- (+ i5 53 (div i5 816)) i9 i2 53 230))) (>= (- i9 i10) (* 49 408 i9))) (= (<= 897 (- (div i5 816) 53 (+ 49 i3)) 53 49) v374 v499) v279 (xor v246 v196) (or (or v1 v1 v5 v0) v6 v6 v2 v0 v9) (distinct (distinct (and v7 v8) v5) (= (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7)) 408))) (< i9 (+ 49 i3) (+ i5 53 (div i5 816)) (- 370 90) (+ 53 49 i7 i7 230) (- (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7)) (- (div i5 816) 53 (+ 49 i3)))) (= (>= 295 418) v394 (distinct v310 (or v46 v29 (> i10 (ufbi3 v2 v0 v7) (+ 53 49 i7 i7 230) 90 406 292) v6) (> (mod i5 810) i5 i7 i3 i8 i2) (> i19 i16) v34 (> i1 (+ 53 49 i7 i7 230) (- 370 90) 53 53 408) v242) (distinct (and v7 v8) (uf3 (= 230 90) (< i17 (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7)) i9 (- 370 90) i19 49) v9) (= (+ 49 i3) (abs 406))) (xor v11 v261 (xor v2 (= v3 v1 v10 v1 v6 v10 v3) v0) (< (mod i5 810) i16) v28)) v57 (xor (> 53 (- i3)) (< (abs 370) 353) v599) v261 (not (or v31 v6 (> i7 (- i9 i10) i1 i2) v8 (and v7 v8) v7 v28))) v61))
 (declare-fun i244 () Int)
 (declare-fun v952 () Bool)
 (push 3)
 (declare-fun v953 () Bool)
 (push 3)
 (declare-fun v954 () Bool)
 (declare-fun v955 () Bool)
 (declare-fun v956 () Bool)
 (declare-fun i245 () Int)
 (declare-fun v957 () Bool)
 (declare-fun i246 () Int)
 (declare-fun v958 () Bool)
 (declare-fun v959 () Bool)
 (declare-fun i247 () Int)
 (declare-fun v960 () Bool)
 (declare-fun v961 () Bool)
 (pop 1)
 (declare-fun v962 () Bool)
 (declare-fun v963 () Bool)
 (declare-fun v964 () Bool)
 (declare-fun v965 () Bool)
 (push 3)
 (declare-fun v966 () Bool)
 (declare-fun v967 () Bool)
 (declare-fun v968 () Bool)
 (declare-fun v969 () Bool)
 (declare-fun v970 () Bool)
 (declare-fun v971 () Bool)
 (declare-fun i248 () Int)
 (declare-fun v972 () Bool)
 (declare-fun i249 () Int)
 (assert (= i166 (div i3 959)))
 (declare-fun v973 () Bool)
 (declare-fun v974 () Bool)
 (declare-fun v975 () Bool)
 (pop 6)
 (declare-fun i250 () Int)
 (push 4)
 (declare-fun v980 () Bool)
 (declare-fun i251 () Int)
 (declare-fun v981 () Bool)
 (push 3)
 (declare-fun v982 () Bool)
 (assert (uf3 (xor (and (uf4 (< (+ i16 i5) 406 (- (- (div i5 816) 53 (+ 49 i3)) (- (div i5 816) 53 (+ 49 i3))) (ufbi3 v2 v0 v7) (div i7 882) (- (+ i5 53 (div i5 816)) i9 i2 53 230)) v242 v268 (=> v53 v31)) (not (or (not (>= 292 230)) (< (+ i16 i5) 406 (- (- (div i5 816) 53 (+ 49 i3)) (- (div i5 816) 53 (+ 49 i3))) (ufbi3 v2 v0 v7) (div i7 882) (- (+ i5 53 (div i5 816)) i9 i2 53 230))))) (uf4 (< (mod i5 810) i16) (not v0) (> (mod i5 810) i5 i7 i3 i8 i2) (or (and v7 v8) v29 v7 (distinct (and v7 v8) v5) v2 (< (mod i5 810) (div i5 816)) (> (mod i5 810) i5 i7 i3 i8 i2))) v8 v246 (distinct S0-0 S0-0 S0-0 S0-0 S0-0)) (and v285 (distinct (+ 53 49 i7 i7 230) (abs i5))) (< (- (+ i1 (- (div i5 816) 53 (+ 49 i3))) (+ (abs 370) (- (+ i5 53 (div i5 816)) i9 i2 53 230) (+ 53 49 i7 i7 230)) 851 716 i9) (ufii6_2 170 406 341 (abs 370) 170 179))))
 (pop 5)
 (declare-fun v983 () Bool)
 (declare-fun v984 () Bool)
 (declare-fun v985 () Bool)
 (declare-fun i252 () Int)
 (declare-fun v986 () Bool)
 (push 1)
 (declare-fun v987 () Bool)
 (pop 2)
 (declare-fun v988 () Bool)
 (declare-fun i253 () Int)
 (pop 1)
 (check-sat-assuming-model (i77 i165 i219) (1627 1012 2174))
 (check-sat-assuming-model (i165 i170) (1495 4023))
 (declare-fun i254 () Int)
 (assert (uf3_2 (= (- 400 694) (* i2 992)) (not (> i1 (+ 53 49 i7 i7 230) (- 370 90) 53 53 408)) v898))
 (declare-fun i255 () Int)
 (declare-fun i256 () Int)
 (declare-fun i257 () Int)
 (declare-fun i258 () Int)
 (assert (xor (or (or v1 v1 v5 v0) v6 v6 v2 v0 v9) (or (= (* (abs i8) 931) 772) (distinct i16 900) v196) (distinct (distinct (and v7 v8) v5) (= (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7)) 408)) (and (distinct v44 v35 (= v44 (and v2 v32 v29 (xor v7 v7) v45 (or v31 v6 (> i7 (- i9 i10) i1 i2) v8 (and v7 v8) v7 v28) v5) (distinct 333 53) v31 (< (mod i5 810) i16) (= i2 (- 370 90))) (> i1 (+ 53 49 i7 i7 230) (- 370 90) 53 53 408) v35 (distinct 370 (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7))) (and v2 v32 v29 (xor v7 v7) v45 (or v31 v6 (> i7 (- i9 i10) i1 i2) v8 (and v7 v8) v7 v28) v5)) (distinct v44 v35 (= v44 (and v2 v32 v29 (xor v7 v7) v45 (or v31 v6 (> i7 (- i9 i10) i1 i2) v8 (and v7 v8) v7 v28) v5) (distinct 333 53) v31 (< (mod i5 810) i16) (= i2 (- 370 90))) (> i1 (+ 53 49 i7 i7 230) (- 370 90) 53 53 408) v35 (distinct 370 (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7))) (and v2 v32 v29 (xor v7 v7) v45 (or v31 v6 (> i7 (- i9 i10) i1 i2) v8 (and v7 v8) v7 v28) v5)) (=> v47 v35) (distinct v2 v5 (distinct 406 i16 i3 49 i17 408))) v271 v598))
 (push 4)
 (declare-fun i259 () Int)
 (declare-fun v997 () Bool)
 (declare-fun i260 () Int)
 (declare-fun i261 () Int)
 (assert (xor (xor (> (mod i5 810) 897) (distinct v2 v5 (distinct 406 i16 i3 49 i17 408)) v46 (< 897 (- (+ i5 53 (div i5 816)) i9 i2 53 230)) (and v2 v32 v29 (xor v7 v7) v45 (or v31 v6 (> i7 (- i9 i10) i1 i2) v8 (and v7 v8) v7 v28) v5)) (or v593 (not v404) (ufib3 (abs 406) 370 (+ 49 370 49 (- i9 i10) (ufbi3 v2 v0 v7))))))
 (check-sat-assuming-model (i5 i171) (3912 3864))
 (check-sat-assuming-model (i17 i171 i220) (924 2067 3662))
 (check-sat-assuming-model (i5 i23 i171) (227 2079 1922))
 (check-sat-assuming-model (i0 i5 i169) (1812 4984 1479))
 (declare-fun S2-2 () S2)
 (declare-fun v998 () Bool)
 (declare-fun v999 () Bool)
 (declare-fun i262 () Int)
 (push 4)
 (declare-fun v1000 () Bool)
 (assert (=> (uf7 v267 (=> v34 v5) v293 (= 878 i15) (or v9 v2 v10 (= v3 v1 v10 v1 v6 v10 v3) v3 v6) v10 v397) v952))
 (check-sat-assuming-model (i81 i165 i205) (4399 1312 4596))
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i77 i78 i81 i112 i113 i114 i115 i116 i117 i118 i132 i139 i142 i151 i159 i160 i165 i166 i167 i168 i169 i170 i171 i172 i173 i192 i195 i205 i218 i219 i220 i221 i222 i229 i230 i231 i235 i236 i237 i243 i244 i250 i254 i255 i256 i257 i258 i259 i260 i261 i262 ) (4082 4648 3300 686 2543 4857 97 1695 3299 2797 2217 3670 959 1429 1852 1607 1359 1749 816 4721 753 4825 115 2121 4833 2353 268 371 3378 2946 3663 3612 2243 4192 2529 3912 841 2408 2201 2856 2232 846 1153 4964 886 874 437 2950 1264 1121 840 1027 3151 3521 909 3308 2707 4422 4462 1621 982 1144 806 2075 2483 123 608 ))
 (check-sat-assuming-model (i5 i244 i262) (1346 4174 2011))
 (check-sat-assuming-model (i17 i117) (3018 3206))
 (declare-fun v1001 () Bool)
 (declare-fun v1002 () Bool)
 (declare-fun i263 () Int)
 (declare-fun i264 () Int)
 (pop 6)
 (declare-fun v1003 () Bool)
 (declare-fun i265 () Int)
 (declare-fun v1004 () Bool)
 (check-sat-assuming-model (i0 i1 i2 i3 i5 i7 i8 i9 i10 i15 i16 i17 i19 i20 i23 i24 i77 i78 i81 i112 i113 i114 i115 i116 i117 i118 i132 i139 i142 i151 i159 i160 i165 i166 i167 i168 i169 i170 i171 i172 i173 i192 i195 i205 i218 i219 i220 i221 i222 i229 i230 i231 i235 i236 i237 i243 i244 i250 i254 i255 i256 i257 i258 i265 ) (4239 4880 4218 1891 510 2866 4689 4976 369 4195 2004 4117 3840 2386 1812 3417 1041 169 2071 4076 934 201 719 4570 4288 1052 3075 2987 3477 4027 2478 3110 2478 1753 2514 2005 31 140 1290 2706 1526 1140 2200 2219 3533 4174 3213 4018 1974 3023 3558 3589 4719 3699 2497 2274 2162 2422 376 462 4573 4934 3558 4738 ))
 (check-sat-assuming-model (i115 i229) (1728 987))
 (check-sat-assuming-model (i173 i222 i265) (2064 1959 1917))
 (declare-fun v1005 () Bool)
 (declare-fun v1006 () Bool)
 (declare-fun v1007 () Bool)
 (declare-fun v1008 () Bool)
 (assert (distinct (> i19 i16) (> 662 494) (>= (abs (abs 406)) 170 (ufii5 i7 (div i17 670) 480 353 823)) (> 53 (- i3)) (< 353 i24) (> (div i5 816) 772) (distinct i16 900)))
 (declare-fun i266 () Int)
 (assert (= (> (- (div i5 816) 53 (+ 49 i3)) 534) v559))
